module book
sig Addr, Name {}
sig Book {
	addr: Name -> (Name + Addr)
	} {
	all n: Name | n not in n.^addr
	}

-- simple case: n is not mapped to
pred pre_del0 (b: Book, n: Name) {
	some b.addr[n] and no b.addr.n
	}
pred del0 (b, b': Book, n: Name) {
	pre_del0 (b, n)
	b'.addr = b.addr - (n->univ)
	}

-- n is mapped to, and can be removed without leaving dangling names
pred pre_del1 (b: Book, n: Name) {
some b.addr.n and all n0: b.addr.n | some x: (Name + Addr) - n | n + x in b.addr[n0]

--	some n0: Name, x: (Name + Addr) - n | n + x in b.addr[n0]
	}
pred del1 (b, b': Book, n: Name) {
	pre_del1 (b, n)
	b'.addr = b.addr - (n->univ) - (univ->n)
	}

-- removing n would leave dangling names
pred pre_del2 (b: Book, n: Name) {
	some n0: Name | b.addr[n0] = n
	}
pred del2 (b, b': Book, n: Name) {
	pre_del2 (b, n)
	b'.addr = b.addr - (n->univ) - (univ->n)
	}

assert delPreCover {
	all b: Book, n: Name |
		pre_del0 (b, n) or pre_del1 (b, n) or pre_del2 (b, n)
	}
check delPreCover for 3 but 1 Book
-- discover case of n not in book at all

assert delPreDisj {
	no b: Book, n: Name |
		(pre_del0 (b, n) and pre_del1 (b, n))
		or (pre_del0 (b, n) and pre_del2 (b, n))
		or (pre_del1 (b, n) and pre_del2 (b, n))
	}
check delPreDisj for 3 but 1 Book
-- disover case of being overlapping for one and not for another
-- fix pre_del1